Skip to content

Conversation

@bugarela
Copy link
Collaborator

@bugarela bugarela commented Sep 5, 2025

  • I have read and I understand the Note on AI-assisted contributions
  • Changes manually tested locally and confirmed to work as described
    (including screenshots is helpful)
  • Tests added for any new code
  • Documentation added for any new functionality
  • Entries added to the respective CHANGELOG.md for any new functionality

@github-actions
Copy link

github-actions bot commented Sep 5, 2025

Benchmark Results

Benchmark Time
evaluator/tictactoe 670.62 µs
evaluator/JMT 43.66 ms
tictactoe/rust 1.50 s
tictactoe/typescript 4.10 s
tuples/rust 1.60 s
tuples/typescript 9.11 s

@romac
Copy link
Contributor

romac commented Sep 5, 2025

What a performance boost! 🚀

@bugarela bugarela changed the title [Rust] oneOf behavior updates and performance improvements [Rust] Change representation of Value for performance improvement Sep 19, 2025
@erickpintor erickpintor force-pushed the gabriela/rust-oneOf-and-perf branch from 298f87c to f80e77b Compare September 30, 2025 11:57
@erickpintor
Copy link
Contributor

I dug a bit on why this change made such a difference, resulting on this compile time assertion here.

The bottom line is: the imbl crate have optimizations that are well suited for small values, often holding them in the stack before creating their internal heap-allocated trees. Previously, Value had a size of 72 bytes in the stack, which forces imbl to start allocating on the heap soon and often. Now the size of Value is 8 bytes, which makes more use of imbl inline stack allocation.

As an experiment, I've replaced the use of ImmutableVec in Value::Tuple with a simple Rust Vec instead and that change alone gives a boost of ~60%:

main:
tuples/rust             time:   [3.8570 s 3.8728 s 3.8897 s]

main (tuples are vectors):
tuples/rust             time:   [1.5432 s 1.5706 s 1.5993 s]
                        change: [-60.113% -59.445% -58.736%] (p = 0.00 < 0.05)
                        Performance has improved.

This serves as further confirmation that imbl was indeed struggling to host values before.

It's worth noting that this patch also promotes some degree of memory fragmentation as simple values like integers (that are cheap to copy) are no longer stack allocated and will get scattered around the heap a lot. However, quint specs aren't as long lived as real programs so, my intuition is that this fragmentation won't impact us that much.

This is all worth considering as we work on this data structures in future iterations of the rust backend, though.

@erickpintor erickpintor marked this pull request as ready for review September 30, 2025 12:50
@bugarela
Copy link
Collaborator Author

Interesting. Switching from native data structures to immutable ones (from imbl) was a huge performance boost when we had the very first version of the rust evaluator. Let's discuss this next week.

@erickpintor erickpintor force-pushed the gabriela/rust-oneOf-and-perf branch from 576dea8 to 5096d33 Compare October 14, 2025 18:52
@bugarela
Copy link
Collaborator Author

After discussing in the meeting, this makes more sense. From what Erick explained, I understood that it could be benefitial to move smaller data structures like tuples from imbl to native vectors due to allocation speed, as tuples won't "grow" over time (growing as in making copies of it with more elements).

@erickpintor I think we are good to merge. You can approve (I can't as I'm the author) and merge it whenever you like

@erickpintor
Copy link
Contributor

Sounds good!

@erickpintor erickpintor merged commit 8af9b1c into main Oct 15, 2025
25 checks passed
@erickpintor erickpintor deleted the gabriela/rust-oneOf-and-perf branch October 15, 2025 18:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants